$\forall$$T$:Type, $L_{1}$, $L_{2}$, $L$:$T$ List, $f_{1}$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$), $f_{2}$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{2}$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$).
\\[0ex]interleaving\_occurence($T$;$L_{1}$;$L_{2}$;$L$;$f_{1}$;$f_{2}$) $\in$ Prop